/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package alloy.api;

import java.io.BufferedReader;
import java.io.PrintWriter;
import java.util.List;
import java.util.Map;

import alloy.ast.Command;
import alloy.ast.Formula;
import alloy.ast.LeafId;
import alloy.ast.Specification;
import alloy.bool.BooleanFormula;
import alloy.transform.FunctionSkolemizer;
import alloy.transl.ASTInfo;
import alloy.transl.TranslInfo;
import alloy.type.BasicType;

/**
 * The interface to a read-only data structure containing
 * information about a solution to a particular
 * {@linkplain alloy.ast.FindCommand command} in an Alloy model.  Returned by
 * {@link AlloyRunner#analyzeCommand} and
 * {@link AlloyRunner#getNextSolution}.
 * <p>
 * Through SolutionData you can access information both about the Alloy formula that was
 * analyzed, and about the instance found by Alloy satisfying the formula.  Note that "Alloy formula"
 * here means the translatable AST -- the completely desugared Alloy {@linkplain alloy.ast.FindCommand#formula formula}
 * for a particular {@linkplain alloy.ast.FindCommand command}.
 * <p>
 * There are two separate ways to access this information via SolutionData.  One involves
 * using some interfaces from packages other than {@link alloy.api}, but may be somewhat
 * cleaner to use; let's call it "direct access".  The other doesn't involve any classes outside
 * of {@link alloy.api} but may be somewhat clumsier; let's call it "wrapped access".  The wrapped
 * access actually uses direct access to get all the data it returns.  Eventually we'll have one interface
 * that combines the best of both.
 * <p>
 * Way 1: Direct access
 * <p>
 * For info about the Alloy formula, call {@link #getTranslator} to get a {@link TranslInfo} object;
 * you can then query it for various information as explained in its documentation.  {@link TranslInfo}
 * is an inteface extending {@link ASTInfo}, so it has methods from both.  {@link ASTInfo} returns information
 * about the Alloy formula: list of all relations in the formula, list of all the basic types used in the
 * formula.  Relations are represented using {@link alloy.ast.LeafId}s, which is an object identifying
 * a given AST {@linkplain alloy.ast.Leaf leaf} and in particular a given relation; so a set of relations
 * is returned as the set of their {@link alloy.ast.LeafId}s.  You can use methods of {@link ASTInfo} to
 * go from leaf id of a relation to its {@linkplain ASTInfo#getLeafType relation type}, and to get a
 * {@linkplain ASTInfo#getLeafRep representative} AST node for this relation from which you can
 * {@linkplain alloy.ast.Node#nodeString get} the name of the relation.
 * <p>
 * You can use methods of {@link TranslInfo} to get the Boolean translation of any AST {@link alloy.ast.Node}.
 * In particular you can get the translation of any relation by passing the relation's {@link LeafId} to
 * {@link TranslInfo#getLeafTransl}.  This will return an {@link alloy.transl.ExprTransl} which is an
 * array of {@link BooleanFormula}s, one for each tuple that the relation may have.  You can get the
 * {@link BooleanFormula} representing the presence of a particular tuple in the relation's value in the solution
 * using {@link alloy.transl.ExprTransl#getTupleFormula} methods.  
 * You can evaluate these Boolean formulas by passing the Boolean assignment found by the SAT solver
 * (returned by {@link #getSolution}) to {@link BooleanFormula#interpret}.   This tells you whether a given
 * tuple of the given relation is present in the solution.
 * <p>
 * The wrapped method of accessing the data: Someone who knows it well please describe it.
 *
 * @see AlloyRunner#translateCommand
 */
public interface SolutionData {

    // SIGNATURES

    /** get a list of all {@link alloy.type.BasicType}s
        seen in this solution */
    public List allTypes();
    
    /** get a list of all String signature names
        corresponding to types seen in the
        formula generated for a command */
    public List allSigs();

    /** get the type of a signature */
    public BasicType typeOfSig(String sigName_);

    /** return <code>true</code> if signature name
        corresponds to a basic sig, <code>false</code>
        otherwise
    */
    public boolean isBasic(String sigName_);
    
    // FIELDS / RELATIONS

    /** get a mapping from all relations to their
        {@link alloy.type.RelationType}s */
    public Map allRelations();
    
    /** given the name of a signature, returns
        a mapping from the signature's String
        fields to their RelationType types */
    public Map fieldsOfSig(String sigName_);

    /** get a list of String[] arrays corresponding
        to all tuples for a given relation: for each tuple in the relation,
	the returned list has String[] element that is an array of
	atom names of atoms in the tuple.  relationName_ must be a fully-qualified
	name. */
    public List tuplesOfRelation(String relationName_);

    // ATOMS
    
    /** given the name of a signature, returns
        a list of String atom names seen in
        the set associated with that signature
        in the solution */
    public List atomsOfSig(String sigName_);

    /** given the name of an atom, returns
        the String signature name associated
        with its type */
    public String typeOfAtom(String atomName_);

    /** given the name of an atom and the
        name of a relation mapping that atom,
        returns a List of String[] arrays
        corresponding to all tuples obtained
        by applying the relation to the atom
        in this solution */
    public List applyRelationToAtom(String atomName_,
                                    String relationName_);

    // SKOLEM CONSTANTS
    
    /** get a Map from the String names of all
        skolem constants to their RelationType
        types */
    public Map skolemConstants();

    /** given the name of a skolem constant, returns
        a List of String[] arrays corresponding to
        the values of the skolem constant in this
        solution */
    public List skolemConstantValues(String skolemName_);

    // ANALYSIS DETAILS (used by Alloy Evaluator)

    /** @return the {@link TranslInfo} which translated the desugared alloy
     {@link alloy.ast.Formula} into a {@link alloy.bool.BooleanFormula}.  the
     {@link TranslInfo} accumulates some useful information during translation
     which can be retrieved afterwards, e.g. {@link TranslInfo#getNodeTranslations},
    {@link TranslInfo#getVarSwitches}, {@link TranslInfo#getRelationTransls}, etc.*/
    public TranslInfo getTranslator();

    /** @return the assignment of values to Boolean variables.  */
    public boolean[] getSolution();

    /** @return the desugared Alloy {@link Formula} we were analyzing. */
    public Formula getFormula();

    /** @return the {@link Command} we were analyzing */
    public Command getCommand();

    /** @return the {@link Specification} containing the (@link Command) we were analyzing **/
    public Specification getSpecification();

    /** 
     * @return FunctionSkolemizer object used to obtain {@link Specification}
     * that contains the command we were analyzing
     **/
    public FunctionSkolemizer getSkolemizer();

    /** @return the translation of the {@link Formula} we were analyzing. */
     BooleanFormula getTranslation();
    
    public String getShortName(String name_);

    /** saves the instance data using a PrintWriter. */
    public void saveInstance (PrintWriter writer);
    
    /** loads the instance data using a BufferedReader. @returns true on success. */
    public boolean loadInstance (BufferedReader reader);

    /** @return the {@link TranslInfo} which translated the desugared alloy
     {@link alloy.ast.Formula} into a {@link alloy.bool.BooleanFormula}.  the
     {@link TranslInfo} accumulates some useful information during translation
     which can be retrieved afterwards, e.g. {@link TranslInfo#getNodeTranslations},
    {@link TranslInfo#getVarSwitches}, {@link TranslInfo#getRelationTransls}, etc.*/
     public ASTInfo getASTInfo();
     
	public alloy.viz.alloyviz.VizInstance getVizInstance();
	
	public void setVizInstance(alloy.viz.alloyviz.VizInstance instance);
	
	public String mapAtomName(String atom);

    /**
     * Return the {@link BasicType} corresponding to Int, or <code>null</code>
     * if Int wasn't used in the model.
     * @see #getIntAtomValue
     */
    public BasicType getIntType();

    /**
     * Get the integer associated with the i'th integer atom.
     * Assumes that integers were used in the model.
     * @param intAtomIdx_ the index of the integer atom; must have
     *        0 <= intAtomIdx_ < getASTInfo().getIntType().getScope().
     * @throws IndexOutOfBoundsException if atom index is invalid or if
     *         integers weren't used in the model.
     @ @see #getIntType
     */
    public long getIntAtomValue(int intAtomIdx_) throws IndexOutOfBoundsException;
}
